$\forall$$T$:Type, $L_{1}$, $L_{2}$:($T$ List), $a$, $b$, $c$:$T$.
\\[0ex]no\_repeats($T$;$L_{2}$)
\\[0ex]$\Rightarrow$ $L_{1}$ $\subseteq$ $L_{2}$
\\[0ex]$\Rightarrow$ adjacent($T$;$L_{1}$;$a$;$b$)
\\[0ex]$\Rightarrow$ adjacent($T$;$L_{2}$;$a$;$c$)
\\[0ex]$\Rightarrow$ ($c$ before $b$ $\in$ $L_{2}$ $\vee$ ($b$ = $c$))